/* Benchmarks for the PionterC */

// get the i-th element, where 0<= i < length (l)

struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==NULL) ||
  @                  (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/
int get_ith(struct list* l, int i)
{
  int j, s;
  struct list* p;
  
  j = 0;
  p = l;
  
  if (l==NULL)
  { s = 0; }
  else
  {
    while (j<i)  /*@ (forall m:int. forall n:int. (({l(->next)n, p}) && ({l(->next)m}) &&  (m!=n))) 
                   @   || (({l, p}) && list (l->next))*/
    {
      j = j+1;
      p = p->next;
    }
    s = p->data;
  }  
  return s;
}
/*@ */

